PRISM
=====
Version: 4.5.dev
Date: Sat Apr 03 05:38:42 CEST 2021
Hostname: christopher
Memory limits: cudd=4g, java(heap)=11g
Command line: prism -javamaxmem 11g -cuddmaxmem 4g -heuristic speed -e 1e-6 -maxiters 1000000 ij.100.prism ij.100.props --property stable
Parsing model file "ij.100.prism"...
Type: MDP
Modules: process0 process1 process2 process3 process4 process5 process6 process7 process8 process9 process10 process11 process12 process13 process14 process15 process16 process17 process18 process19 process20 process21 process22 process23 process24 process25 process26 process27 process28 process29 process30 process31 process32 process33 process34 process35 process36 process37 process38 process39 process40 process41 process42 process43 process44 process45 process46 process47 process48 process49 process50 process51 process52 process53 process54 process55 process56 process57 process58 process59 process60 process61 process62 process63 process64 process65 process66 process67 process68 process69 process70 process71 process72 process73 process74 process75 process76 process77 process78 process79 process80 process81 process82 process83 process84 process85 process86 process87 process88 process89 process90 process91 process92 process93 process94 process95 process96 process97 process98 process99
Variables: q0 q1 q2 q3 q4 q5 q6 q7 q8 q9 q10 q11 q12 q13 q14 q15 q16 q17 q18 q19 q20 q21 q22 q23 q24 q25 q26 q27 q28 q29 q30 q31 q32 q33 q34 q35 q36 q37 q38 q39 q40 q41 q42 q43 q44 q45 q46 q47 q48 q49 q50 q51 q52 q53 q54 q55 q56 q57 q58 q59 q60 q61 q62 q63 q64 q65 q66 q67 q68 q69 q70 q71 q72 q73 q74 q75 q76 q77 q78 q79 q80 q81 q82 q83 q84 q85 q86 q87 q88 q89 q90 q91 q92 q93 q94 q95 q96 q97 q98 q99 num_tokens_var
Parsing properties file "ij.100.props"...
1 property:
(1) "stable": Pmax=? [ F ((q0+q1+q2+q3+q4+q5+q6+q7+q8+q9+q10+q11+q12+q13+q14+q15+q16+q17+q18+q19+q20+q21+q22+q23+q24+q25+q26+q27+q28+q29+q30+q31+q32+q33+q34+q35+q36+q37+q38+q39+q40+q41+q42+q43+q44+q45+q46+q47+q48+q49+q50+q51+q52+q53+q54+q55+q56+q57+q58+q59+q60+q61+q62+q63+q64+q65+q66+q67+q68+q69+q70+q71+q72+q73+q74+q75+q76+q77+q78+q79+q80+q81+q82+q83+q84+q85+q86+q87+q88+q9+q90+q91+q92+q93+q94+q95+q96+q97+q98+q99)=1) ]
---------------------------------------------------------------------
Model checking: "stable": Pmax=? [ F ((q0+q1+q2+q3+q4+q5+q6+q7+q8+q9+q10+q11+q12+q13+q14+q15+q16+q17+q18+q19+q20+q21+q22+q23+q24+q25+q26+q27+q28+q29+q30+q31+q32+q33+q34+q35+q36+q37+q38+q39+q40+q41+q42+q43+q44+q45+q46+q47+q48+q49+q50+q51+q52+q53+q54+q55+q56+q57+q58+q59+q60+q61+q62+q63+q64+q65+q66+q67+q68+q69+q70+q71+q72+q73+q74+q75+q76+q77+q78+q79+q80+q81+q82+q83+q84+q85+q86+q87+q88+q9+q90+q91+q92+q93+q94+q95+q96+q97+q98+q99)=1) ]
Warning: Switching to sparse engine and (backwards) Gauss Seidel (default for heuristic=speed).
Building model...
Computing reachable states...
Reachability (BFS): 100 iterations in 0.21 seconds (average 0.002060, setup 0.00)
Time for model construction: 0.836 seconds.
Type: MDP
States: 1.2676506002282294E30 (1 initial)
Transitions: 1.1091942751997007E32
Choices: 6.338253001141147E31
Transition matrix: 22177 nodes (3 terminal), 1.1091942751997007E32 minterms, vars: 107r/107c/99nd
Warning: Switching to MTBDD engine, as number of states is too large for Sparse engine.
Prob0A: 99 iterations in 1075.55 seconds (average 10.864141, setup 0.00)
----------
Computation aborted after 1800.093122959137 seconds since the total time limit of 1800 seconds was exceeded.